A, B:RealizerScheme{i:l}. scheme-compatible{i:l}(A; B)  {i'} 

latex

Definitions	t  T, {x:A| B(x)} , , type List, x:AB(x), Namer(n;Id_list), x:A. B(x), Id, A  B, A  B, P  Q, [], <a, b>, s = t, False, A, , True, T, namer-disjoint(n1;n2;nmr1;nmr2), {i..j}, P & Q, i  j < k, Inj(A;B;f), f(a), Atom$n, (x  l), Type, ||as||, l[i], A c B, x:A  B(x), a < b, , P  Q, P  Q, Void, #$n, A || B, Realizer, let x,y,z = a in t(x;y;z), scheme-compatible(A;B), RealizerScheme{i:l}()
Lemmas	Id wf, es realizer wf, R-compat wf, int seg wf, inject wf, not wf, namer-disjoint wf, nat wf, length wf2, false wf, not functionality wrt iff, nil member, select wf, l member wf, Namer wf, Namer-subtype, l contains nil